(set-logic QF_RDL)
(set-info :source | SMT-COMP'06 Organizers |)
(set-info :smt-lib-version 2.0)
(set-info :category "check")
(set-info :status unsat)
(set-info :notes |This benchmark is designed to check if the DP supports bignumbers.|)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun x3 () Real)
(declare-fun x4 () Real)
(assert (and (< (- x1 x2) (/ 1 1000000000000000000000000000000000)) (< (- x2 x3) (/ 1 2000000000000000000000000000000011)) (< (- x3 x4) (/ (- 1) 1000000000000000000000000000000000)) (< (- x4 x1) (/ (- 1) 1999999999999999999999999999999988))))
(check-sat)
(exit)
